$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$($B$ + Top)), $P$:($A$$\rightarrow\mathbb{P}$), $p$:($\forall$$x$:$A$. Dec($P$($x$))), $x$:$A$.
\\[0ex]($\uparrow$can{-}apply(p{-}restrict($f$;$p$);$x$)) $\Leftarrow\!\Rightarrow$ (($\uparrow$can{-}apply($f$;$x$)) \& $P$($x$))